Peano playground
Peano axioms
0 is N
a=b
a=b & b=c -> a=c
a=b & b is N -> a is N
a is N -> S(a) is N
S(a)=S(b) -> a=b
S(a)!=0
0 is K & (a is K -> S(a) is K) -> a is K
Note: '&' has more priority than '->'
Note: 'S' is a function
TODO: plus
TODO: times
TODO: prime
Theorems
1+1 = 2
2 is prime
3 is prime
Euclid's lemma
Fundamental theorem of arithmetics